package ch.epfl.lara.matcheck.verify.axioms;

import ch.epfl.lara.matcheck.ast.{Set,In,LessEq,Less,Forall,Imply,Or}

trait PredefAxioms extends IAxiom 
                   with    Predefined 
		   with    PropositionalFormulaMaker
{
  import ifc._
  private var _predefined: Axiom = conjunction(integers :: Nil)
  
  private def integers: Axiom = {
    val x = "x"
    val int = Set(INT_SET)
    Forall(x,Imply(In(x,int),Or(LessEq(0,x),Less(x,0))))
  }

  def predefined: Axiom = _predefined
}
